A Process Algebra for Wireless Mesh Networks used for Modelling, Verifying and Analysing AODV

摘要

We propose AWN (Algebra for Wireless Networks), a process algebra tailored tothe modelling of Mobile Ad hoc Network (MANET) and Wireless Mesh Network (WMN)protocols. It combines novel treatments of local broadcast, conditional unicastand data structures. In this framework we present a rigorous analysis of the Ad hoc On-DemandDistance Vector (AODV) protocol, a popular routing protocol designed for MANETsand WMNs, and one of the four protocols currently standardised by the IETFMANET working group. We give a complete and unambiguous specification of this protocol, therebyformalising the RFC of AODV, the de facto standard specification, given inEnglish prose. In doing so, we had to make non-evident assumptions to resolveambiguities occurring in that specification. Our formalisation models the exactdetails of the core functionality of AODV, such as route maintenance and errorhandling, and only omits timing aspects. The process algebra allows us to formalise and (dis)prove crucial propertiesof mesh network routing protocols such as loop freedom and packet delivery. Weare the first to provide a detailed proof of loop freedom of AODV. In contrastto evaluations using simulation or model checking, our proof is generic andholds for any possible network scenario in terms of network topology, nodemobility, etc. Due to ambiguities and contradictions the RFC specificationallows several interpretations; we show for more than 5000 of them whether theyare loop free or not, thereby demonstrating how the reasoning and proofs canrelatively easily be adapted to protocol variants. Using our formal and unambiguous specification, we find shortcomings of AODVthat affect performance, e.g. the establishment of non-optimal routes, and someroutes not being found at all. We formalise improvements in the same processalgebra; carrying over the proofs is again easy.